\section{Other VCC Features}


\subsection{BVD (main text)}
\subsection{addr-eq(), addr()}
\subsection{arrays-disjoint}
\subsection{begin-update}
\subsection{start-here}
\subsection{Using pure functions for triggering}
\subsection{Frame axioms}
\subsection{extent-mutable and friends}
\subsection{Claim upgrade}
\subsection{by-claim}
\subsection{Approvers}
\subsection{set operations}
\subsection{Volatile domains (?)}
\subsection{Globals}
\subsection{Groups}
\subsection{Structure inlining + backing member}
\subsection{Structure equality}
\subsection{Out parameters}
\subsection{Skinny expose}
\subsection{Mathint}
\subsection{Allocating ghost objects}
\subsection{Smoke}
\subsection{known (?)}
\subsection{Isabelle}
